AGDA_FAILURE

ret > ExitFailure 42
out > Issue5007-sizedtypes.agda:33,32-36
out > I'm not sure if there should be a case for the constructor refl,
out > because I get stuck when trying to solve the following unification
out > problems (inferred index ≟ expected index):
out >   x .D′.force
out >   (_j_37 (i = i) (x′ = x′) (y′ = y′) (x = x) (y = y)) ≟ x′
out > when checking that the pattern refl has type
out > x .D′.force (_j_37 (i = i) (x′ = x′) (y′ = y′) (x = x) (y = y)) ≡
out > x′
out >
